Inference at * 2 
Iof proof for Lemma assert of bnot:



1. p : 
  ((p))  ((p)) 

latex

 by ((((BoolInd 1) 
CollapseTHEN (((Unfolds ``assert bnot not`` 0) 
CollapseTHEN (Rewrite (
CRepeatC (HigherC ifthenelse_evalC)) 0))))) 
CollapseTHEN ((Auto_aux (first_nat 1:n
C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1: 1. True  False
C1:   False
C.

Definitions	, P  Q, True, ff, if b then t else f fi , tt, t  T, A, b, b, P  Q, False, Unit, ,
Lemmas	false wf, true wf